Skip to content

docs(fv): update README to .conf-based specs and correct run syntax #6120

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

docs(fv): update README to .conf-based specs and correct run syntax #6120

wants to merge 1 commit into from
+6 −6

Conversation

@sashass1315
Copy link
Contributor

@sashass1315 sashass1315 commented Nov 16, 2025

The formal verification workflow uses per-spec .conf files in fv/specs/ alongside .spec files, and the runner fv/run.js discovers fv/specs/*.conf and only supports --all, --parallel/-p, and --verbose/-v. The README referenced specs.json/spec.json and implied passthrough of arbitrary CLI options which do not exist in the current implementation and CI. This change aligns the README with the actual code and CI by documenting .conf usage, fixing the invocation syntax, clarifying SPEC_NAME mapping to fv/specs/SPEC_NAME.conf, and correcting the example comment to reference the configuration, harness, and spec.

@sashass1315 sashass1315 requested a review from a team as a code owner November 16, 2025 16:43
@changeset-bot
Copy link

changeset-bot bot commented Nov 16, 2025

⚠️ No Changeset found

Latest commit: dd5ecd6

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

@coderabbitai
Copy link
Contributor

coderabbitai bot commented Nov 16, 2025

Walkthrough

The fv/README.md file is updated to reflect a new specification sourcing and selection mechanism. The documentation shifts from referencing a global specs.json entry to per-spec .conf files located in fv/specs/. The run command syntax is extended to accept either a SPEC_NAME or explicit fv/specs/NAME.conf path. Command options (--all, --parallel/-p, --verbose/-v) are expanded and clarified. Example usage and explanations are adjusted to demonstrate selecting specs by configuration file name rather than spec key from specs.json.

Possibly related PRs

Suggested labels

ignore-changeset

Pre-merge checks and finishing touches

✅ Passed checks (3 passed)
Check name Status Explanation
Title check ✅ Passed The title directly and accurately summarizes the main change: updating the README documentation for formal verification to reflect .conf-based specs and correcting the run syntax.
Description check ✅ Passed The description clearly relates to the changeset by explaining why the README was updated—to align it with the actual implementation and CI, documenting .conf usage and correcting outdated references.
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
✨ Finishing touches
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Post copyable unit tests in a comment
📜 Recent review details

Configuration used: CodeRabbit UI

Review profile: CHILL

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between 6308fdc and dd5ecd6.

📒 Files selected for processing (1)
  • fv/README.md (1 hunks)
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (9)
  • GitHub Check: Redirect rules - solidity-contracts
  • GitHub Check: coverage
  • GitHub Check: tests-upgradeable
  • GitHub Check: slither
  • GitHub Check: tests-foundry
  • GitHub Check: halmos
  • GitHub Check: tests
  • GitHub Check: Header rules - solidity-contracts
  • GitHub Check: Pages changed - solidity-contracts
🔇 Additional comments (4)
fv/README.md (4)

16-16: LGTM!

Clear and accurate documentation of the per-spec .conf file approach.

23-23: Clarify the -p N parameter syntax and document flag behaviors.

The command syntax line could be clearer about -p N: should it be -p N, -pN, or -p=N? Additionally, documenting what each flag does (--all, -p/--parallel, -v/--verbose) would improve usability.

Please verify the exact syntax and behavior of these flags by checking fv/run.js. For example:

  • Does --all run all specs vs. a single spec?
  • What does -p or --parallel do, and does it require a value?
  • What does -v or --verbose do?

You can optionally enhance the documentation with brief descriptions once verified.

28-30: LGTM!

The explanation of SPEC_NAME mapping and alternative explicit path is clear and well-documented with an example.

38-38: LGTM!

Clear example that correctly demonstrates the SPEC_NAME mapping to the configuration file.

Tip

📝 Customizable high-level summaries are now available!

You can now customize how CodeRabbit generates the high-level summary in your pull requests — including its content, structure, tone, and formatting.

  • Provide custom instructions to shape the summary (bullet lists, tables, contributor stats, etc.).
  • Use high_level_summary_in_walkthrough to move the summary from the description to the walkthrough section.

Example:

"Create a concise high-level summary as a bullet-point list. Then include a Markdown table showing lines added and removed by each contributing author."

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands and usage tips.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@sashass1315